change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs #487
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
5a4a8ea to
0a11a30
Compare
affeldt-aist
changed the title
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
0a11a30 to
b426af7
Compare
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
3 times, most recently
from
55724fb to
919efcc
Compare
|
IIRC, the problem with this PR is that it does not bring the expected code size reduction. But there is now code size augmentation (except with one lemma). Since we all seem to agree that large inequalities fell better suited, we can maybe merge this PR for now. What do you think? |
|
I think this PR essentially exibits a lack of abstraction. We should actually understand how to make the code smaller, and I think it might not be about changing the def. |
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
7fbcf48 to
5929a80
Compare
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
5929a80 to
cc6d238
Compare
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
3 times, most recently
from
afd2f59 to
cdacbaf
Compare
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
cdacbaf to
a811911
Compare
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
a811911 to
1c54ead
Compare
proux01
added
the
TODO: MC2 port
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
2 times, most recently
from
b719baa to
2b10bdc
Compare
|
NB: after a rebase on MathComp 1.3.1, the proofs of the lemmas |
affeldt-aist
removed
the
TODO: MC2 port
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
6 times, most recently
from
572778e to
3b9c43b
Compare
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
3b9c43b to
26740c7
Compare
- from strict to large
- also in {p,n}infty_{d,}nbhs
closed #122
affeldt-aist
force-pushed
the
ereal_dnbhs_nbhs
branch
from
26740c7 to
a0e6d38
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
ereal.vclosed #122 @CohenCyril
This is globally getting a bit bigger (only a few proofs are shortened).
I have maybe not been careful enough when updating.